r:CRng, a:Ideal(r){i}, d:detach_fun(|r|;a). |r|  Carrier(r/d) 

latex

Definitions	x:A. B(x), S  T, t  T, Carrier(r/d), x f y, Prop, x,y. t(x;y), CRng, Ideal(r){i}, Rng, detach_fun(T;A), P  Q, x(s1,s2)
Lemmas	rng car wf, detach fun wf, ideal wf, crng wf, quotient qinc, assert wf, rng plus wf, rng minus wf, det ideal defines eqv